-- -- Copyright 2014 Alessandro Gerlinger Romero -- -- This file is part of Hybrid fUML. -- -- Hybrid fUML is free software: you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation, either version 3 of the License, or -- (at your option) any later version. -- -- Hybrid fUML is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with Hybrid fUML. If not, see . -- ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- Module: semanticMapping_main -- Import: syntax_abstractSyntax_embedded -- Import: syntax_abstractSyntax_profile -- Import: syntax_abstractSyntax_derivedFunctions -- Import: syntax_library_embedded -- Import: syntax_userModel_embedded -- Import: semanticDomain_embedded -- Import: semanticDomain_defined -- Import: semanticMapping ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- MAIN RULE rule_fUML_mainHyb :: Rule() rule_fUML_mainHyb = if not (emptyDom function_fUML_Agents) then -- (R) REACTION -- (RA) prepare reaction rule_fUML_prepareReactionHyb `seq` -- (RB) iteration to support the search for a fixpoint between the interaction of continuous and discrete behaviors iterate ( -- (D) DISCRETE -- (DA) prepare a discrete step rule_fUML_prepareDiscreteStepHyb `seq` ( -- (DB) it tests: discrete behavior evaluation should be done if function_fUML_executeDiscreteSteps l then -- (DC) evaluate discrete behavior until fix point iterate (multiDeterm function_fUML_Agents) else skip ) `seq` -- (DD) check result from discrete computation rule_fUML_checkDiscreteStepsHyb `seq` -- (C) CONTINUOUS -- (CA) iteration iterate ( -- (CB) define system of equations for each active object rule_fUML_defineEquations `seq` -- (CC) compute the system of equations for each active object rule_fUML_computeEquations `seq` -- (CD) check the right edge rule_fUML_checkEdge ) ) `seq` -- (RC) check result from continuous computation rule_fUML_checkContinuousEvolutionForReaction else skip where -- locus l = function_fUML_locus ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- INIT RULE -- create an agent for the activity main (must exist) -- receives -- reaction time -- discretizationstep -- evolveAutomatically -- used to define the reaction time and discretization step without parsing the CCSLs -- SIMULATION rule_fUML_initSim :: Int -> Float -> Rule() rule_fUML_initSim rt ds = rule_fUML_init rt ds True -- used to hybrid behavior defined by clock constraints without explicit reception of signal related with reactionClk -- TIMED MODE rule_fUML_initTimed :: Rule() rule_fUML_initTimed = rule_fUML_init 0 0.0 True -- TIMED MODE - with time control under model, i.e. the model generates signals related with time rule_fUML_initTimed2 :: Rule() rule_fUML_initTimed2 = rule_fUML_init 0 0.0 False -- used to hybrid behavior based on logical clock with not predefined period or discretization step... so the user must inform the discretization step and the period is -1 -- FUNDAMENTAL - for the zero-crossing mode -- it determines that the semantics are waiting for a signal related with reaction to terminate a reaction, and it can evolve time forever... -- -- EVENT (ZERO-CROSSING MODE) rule_fUML_initEvent :: Float -> Rule() rule_fUML_initEvent ds = rule_fUML_init (-1) ds True ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- PREPARE NEW REACTION rule_fUML_prepareReactionHyb :: Rule() rule_fUML_prepareReactionHyb = do rule_fUML_prepareReaction -- reset hybrid trace forall o <- (expr2list function_fUML_activeObjects) do function_fUML_hybridTrace(o):= [] `seq` -- indicating that edge should be verified function_Locus_physicalClkIsOnEdge(l):= False where -- locus l = function_fUML_locus -- rc = function_Locus_reactionClock l ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- PREPARE NEW DISCRETE STEP rule_fUML_prepareDiscreteStepHyb :: Rule() rule_fUML_prepareDiscreteStepHyb = -- create new agents for satisfied discrete domain -- for active objects with classifierBehavior alive rule_fUML_evaluateDiscreteDomains `seq` rule_fUML_prepareDiscreteStep ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- CHECK -- check if discrete steps reached a fixpoint with a meanningful result -- 1. there are no clock that generates conflict... otherwise it is impossible to define the physical time to be covered -- 2. there is a tick for a clock related with the reactionClk (logical evolution) -- -- define the physical time evolution to satisfy the clock (if applicable) rule_fUML_checkDiscreteStepsHyb :: Rule() rule_fUML_checkDiscreteStepsHyb = -- -- there is no logical timebase desynchronized (no event in the current reaction) -- so there is no evolution on time if ctbdsl == 0 then skip else -- there are logical timebases desynchronized do -- check if should evolve physical clock -- it does not workg for zerocrossing mode if shallTick && not (function_Locus_physicalClkIsOnEdge l) && not (function_fUML_isZeroCrossingMode l) then do -- other ticks are checked and generate physical desynchronization if not cpte then -- if physical time is evolving and there is a event related with time, there is a problem with the clocks schedule error("rule_fUML_checkDiscreteSteps - Clock synchronization problem. Maximum: " ++ show (maximum pte) ++ " Minium: " ++ show (minimum pte) ++ " PhysicalClock is Synchronized: " ++ show pcs ++ " physical time: " ++ show pt ++ " active clocks: " ++ show ptee ++ " Max value for clocks: " ++ show pte) else skip -- are the number of instants wrong? if not cpte2 then error("rule_fUML_checkDiscreteSteps - Clock synchronization problem. Calculated instants are not correct! Expected: " ++ show (minimum minP) ++ " Calculated: " ++ show (length nt) ++ " active clocks: " ++ show ptee ++ " Max value for clocks: " ++ show pte ++ " Instants: " ++ show (nt)) else skip -- creating new instants for physical clock forall x <- nt do ri <- (rule_FUML_Semantics_Extensions_Clock_Instant_create FUML_Semantics_Extensions_Clock_JunctionInstant) function_Instant_date(ri) := x function_Instant_tb(ri):=ptb -- stdout rule_fUML_out $ "rule_fUML_checkDiscreteSteps - Physical time: " ++ show pt ++ " Instants: " ++ show (nt) ++ " clocks: " ++ show ptee ++ " logical time: " ++ show (function_fUML_Clock_currentTimeInt lc) else skip -- if physical time should evolve but reaction is on edge if shallTick && function_Locus_physicalClkIsOnEdge l then error("rule_fUML_checkDiscreteSteps - Clock synchronization problem. It is received an event to evolve physicalClk on the edge. Maximum: " ++ show (maximum pte) ++ " Minium: " ++ show (minimum pte) ++ " PhysicalClock is Synchronized: " ++ show pcs ++ " physical time: " ++ show pt ++ " active clocks: " ++ show tbdslp ++ " Instants for clocks: " ++ show pte) else skip -- if it is in the zerocrossingmode if function_fUML_isZeroCrossingMode l then -- check for a clock that determines an edge if not (function_Locus_physicalClkIsOnEdge l) && not shallTick then -- it looks for a clock that is related with reaction clock and it is different from reactionClk let clocksRelatedReaction = filter (\c -> function_fUML_Clock_isRelatedWithReactionClk c && c /= rc) tbdsl in let clocksToShow = map (\cl -> function_Clock_LogicalClock_definingEvent cl) clocksRelatedReaction in do if length clocksRelatedReaction > 0 then do -- if found then it is the edge of the physicalClock evolution function_Locus_physicalClkIsOnEdge(l):= True -- it guarantees that physicalClock is synchronized removing the last element if not (function_fUML_isOnEdgePhysicalClock ptb) then let i = last (function_TimeBase_instants ptb) in do function_Instant_date(i) := 0.0 function_Instant_tb(i):= FUML_Semantics_Extensions_Clock_TimeBaseEmpty else skip -- stdout rule_fUML_out $ "rule_fUML_checkDiscreteSteps - DEFINED EDGE IN THE EVENT MODE. Physical time: " ++ show pt ++ " logical time: " ++ show (function_fUML_Clock_currentTimeInt lc) ++ " clocks: " ++ show clocksToShow else skip else -- increments the clock for the initial time if not (function_Locus_physicalClkIsOnEdge l) && shallTick then do -- creating new instant for physical clock -- one step considering the resolution ri <- (rule_FUML_Semantics_Extensions_Clock_Instant_create FUML_Semantics_Extensions_Clock_JunctionInstant) function_Instant_date(ri) := function_fUML_Clock_currentTimeFloat pc + function_Clock_resolution pc function_Instant_tb(ri):=ptb else skip else skip -- synchronize all timebases forall c <- tbdsl do function_TimeBase_currentInstant(function_Clock_timeBase c) := last (function_TimeBase_instants (function_Clock_timeBase c)) where -- locus l = function_fUML_locus -- rc = function_Locus_reactionClock l rt = function_fUML_Clock_currentTimeInt rc rtb = function_Clock_timeBase rc pc = function_Locus_physicalClock l pt = function_Clock_currentTime pc ptb = function_Clock_timeBase pc lc = function_Locus_logicalClock l -- time stsi = function_Clock_resolution pc -- pc is synchronized pcs = function_fUML_isOnEdgePhysicalClock ptb -- all logical clocks clocks = function_Locus_logicalClocks l -- -- defining if it has logical clock not pointing to the current instant tbdsl = filter (\cl -> function_fUML_Clock_isDesynchronized cl) $ expr2list clocks ctbdsl = length tbdsl -- -- filtering clocks related with physicalClk tbdslp = filter (\cl -> function_fUML_Clock_isRelatedWithPhysicalClk cl ) tbdsl ctbdslp = length tbdslp -- filtering clocks with currentTime greather than 0 tbdslpf = filter (\cl -> getTimeConsideringReactionClk cl > 0 ) tbdslp getTimeConsideringReactionClk c = if c == rc then (function_fUML_Clock_currentTimeInt c) - 1 else (function_fUML_Clock_currentTimeInt c) shallTick = length tbdslpf > 0 -- proposed last physical time pte = map (\cl -> fromInteger ( (getTimeConsideringReactionClk cl) * (function_fUML_Clock_getPeriodWithDefault cl)) * (function_Clock_resolution pc)) tbdslpf -- as reaction time starts from 1, it should be evaluated here pte1 = head pte -- check proposed time: it should lead to the same value, it should be bigger than current pt, and it should not have pending steps in pt cpte = maximum pte == minimum pte && pte1 > pt && pcs -- minP = map (\cl -> function_fUML_Clock_getPeriodWithDefault cl) tbdslpf cpte2 = minimum minP == length nt -- new time instants -- VERY STRANGE, but: [0.7,0.7+0.1..0.8] => [0.7, 0.8] HOWEVER, [0.6,0.6+0.1..0.7] => [0.6] -- SO I DEFINED A MINOR DIFFERENCE IN THE UPPER BOUND nt = (init $tail [pt,pt+stsi..(pte1+(stsi/2.0))]) ++ [pte1] -- -- ptee = map (\cl -> function_Clock_LogicalClock_definingEvent cl) tbdslp ptea = map (\cl -> function_Clock_LogicalClock_definingEvent cl) tbdsl ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- CHECK EDGE -- it defines the edge flag on the locus -- this flag determines that evolution of time is finished -- rule_fUML_checkEdge :: Rule() rule_fUML_checkEdge = do -- garbage collector rule_fUML_garbageCollector if not (function_Locus_physicalClkIsOnEdge l) then -- if it is working on the zero-crossing mode then time should always evolve if function_fUML_isOnEdgePhysicalClock ptb && function_fUML_isZeroCrossingMode l then do -- creating new instant for physical clock -- one step considering the resolution -- in this case the edge is defined by a discrete condition checked in the "rule_fUML_checkDiscreteSteps" ri <- (rule_FUML_Semantics_Extensions_Clock_Instant_create FUML_Semantics_Extensions_Clock_JunctionInstant) function_Instant_date(ri) := function_fUML_Clock_currentTimeFloat pc + function_Clock_resolution pc function_Instant_tb(ri):=ptb -- removing the instant in the beginning of the array of instants if length (function_TimeBase_instants ptb) == 2 then let ir = head (function_TimeBase_instants ptb) in do function_Instant_date(ir) := 0.0 function_Instant_tb(ir):= FUML_Semantics_Extensions_Clock_TimeBaseEmpty else skip else if function_fUML_isOnEdgePhysicalClock ptb then do function_Locus_physicalClkIsOnEdge(l):= True -- stdout rule_fUML_out $ "rule_fUML_checkDiscreteSteps - DEFINED EDGE IN THE TIMED MODE. Physical time: " ++ show (function_fUML_Clock_currentTimeFloat pc) else skip else skip where -- locus l = function_fUML_locus -- pc = function_Locus_physicalClock l ptb = function_Clock_timeBase pc rc = function_Locus_reactionClock l rt = function_fUML_Clock_currentTimeInt rc ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- -- CHECK -- Check continuous evolution the physical time should be synchronized rule_fUML_checkContinuousEvolutionForReaction :: Rule() rule_fUML_checkContinuousEvolutionForReaction = if not isOnEdgePhysicalClock then -- if physical time is synchronized (last == current) -- means that time should evolve but there is no equation enabled -- chose to treat as error error("rule_fUML_checkContinuousEvolutionForReaction - Clock synchronization problem. Time should evolve but it has not evolved.") else skip where -- locus l = function_fUML_locus -- pc = function_Locus_physicalClock l ptb = function_Clock_timeBase pc isOnEdgePhysicalClock = function_fUML_isOnEdgePhysicalClock ptb ------------------------------------------------------------------------------------------------------------------------------------------------------------ -- SUPPORT FUNCTIONS -- -- used to check if it is working on the mode zero-crossing to detect end of reaction -- -- if the reaction clock has no relation with physicalclock and defaultPeriod is -1 -- then is zero crossing, and -1 determines that the physical time does not stop to evolve until a signal associated with reaction function_fUML_isZeroCrossingMode :: FUML_Semantics_Loci_LociL1_Locus -> Bool function_fUML_isZeroCrossingMode l = let rc = function_Locus_reactionClock l in let defaultPeriod = function_Locus_defaultPeriod2ReactionClk l in if function_fUML_Clock_getPeriod rc == 0 && defaultPeriod == -1 then True else False